Various methods are known in the art for verifying complex hardware and logic designs. Some verification applications (commonly referred to as model checking methods) model the design as a finite state machine and express the hardware specification in temporal logic. For many designs, the number of states in such state machine can be prohibitive, and the explicit traversal of the state space becomes infeasible. To reduce the number of states, some applications use symbolic model checking methods, which encode the finite state machine in terms of Boolean formulas. Some symbolic model checking methods use binary decision diagrams (BDDs) for representing Boolean formulas. BDDs are described, for example, by Bryant in “Graph-based Algorithms for Boolean Function Manipulation,” IEEE Transactions on Computers, (35:8), August 1986, pages 677-691.
Bounded Model Checking (BMC) is a symbolic model checking method introduced by Biere et al. in “Symbolic Model Checking Without BDDs,” Tools and Algorithms for the Construction and Analysis of Systems Fifth International Conference (TACAS'99) volume 1579 of Lecture Notes in Computer Science, July 1999, pages 193-207. Bounded model checking is based on propositional satisfiability (SAT) procedures. The method considers counterexamples of a particular length and generates a propositional formula that is satisfiable if and only if such a counterexample exists. The authors show that bounded model checking for linear temporal logic (LTL) can be reduced to propositional satisfiability in polynomial time.
Many satisfiability solving methods are based on variants of the well-known Davis-Putnam-Longman-Loveland (DPLL) algorithm, which is described by Davis et al. in “A machine program for theorem-proving,” Communications of the ACM, (5:7), pp. 394-397, July 1962.
Various methods and software tools are known in the art for solving propositional satisfiability (SAT) problems. For example, Merques-Silva and Sakallah describe a SAT solver called GRASP (Generic seaRch Algorithm for the Satisfiability Problem) in “GRASP: A Search Algorithm for Propositional Satisfiability,” IEEE Transactions on Computers, (48:5), May 1999, pages 506-521.
Another SAT solver is described by Moskewicz et al. in “Chaff: Engineering an Efficient SAT Solver,” Proceedings of the 38th Annual IEEE/ACM Design Automation Conference (DAC'2001), Las Vegas, Nev., June 2001.
Goldberg and Novikov describe a tool called BerkMin in “BerkMin: A Fast and Robust SAT Solver,” Proceedings of the Design Automation and Test in Europe (DATE'2002) Conference, Paris, France, March 2002, pages 142-149.
Yet another SAT solver called SATO is described by Zhang in “SATO: An Efficient Propositional Prover,” Proceedings of the 14th International Conference on Automated Deduction, Townsville, Australia, July 1997, pages 272-275.
Nudelman et al. describe a tool called SATzilla, which aggregates several SAT solvers, in “SATzilla: An Algorithm Portfolio for SAT,” SAT 2003 Competition, in conjunction with the Sixth International Conference on the Theory and Applications of Satisfiability Testing. SATzilla is a portfolio of SAT algorithms (including, for example, SATO and BerkMin cited above). The authors describe a method that predicts the running time of each algorithm for a given SAT instance and runs the algorithm predicted to be fastest.
In some cases, SAT solvers use heuristics and learning techniques for reducing the time and memory requirements of the solving process. For example, The BerkMin SAT solver cited above uses decision-making procedures, non-chronological backtracking, conflict analysis and clause database management as part of the solving process.
Several learning techniques and decision strategies are described by Ryan in “Efficient Algorithms for Clause-Learning SAT Solvers,” M. Sc. Thesis, Simon Fraser University, Burnaby BC, Canada, February 2004.
Lagoudakis and Littman describe a method for choosing appropriate branching rules in a DPLL SAT solver in “Learning to Select Branching Rules in the DPLL Procedure for Satisfiability,” Electronic Notes in Discrete Mathematics (ENDM), Volume 9, LICS 2001 Workshop on Theory and Applications of Satisfiability Testing (SAT 2001), Boston, Mass., June 2001. The method uses a reinforcement-learning approach, in which a value function, which predicts the performance of each branching rule in each case, is learned through trial runs on a typical problem set of the target class of SAT problems.
Bayardo and Schrag describe a method that incorporates constraint satisfaction problem (CSP) look-back techniques to enhance the Davis-Putnam procedure in “Using CSP Loop-Back Techniques to Solve Real-World SAT Instances,” Proceedings of the 14th National Conference on Artificial Intelligence, Providence, R.I., July 1997, pages 203-208.
Herbstritt and Becker describe another method for branching rule selection in “Conflict-Based Selection of Branching Rules,” Proceedings of the Sixth International Conference on Theory and Application in Satisfiability Testing (SAT'2003), Santa Margherita Ligure, Italy, May 2003, pages 441-451. The method uses a set of branching rules. Each branching rule is given a preference value, which models the probability of selecting the branching rule. The preference values are dynamically adapted with respect to conflict analysis. Learning methods and decision strategies are also described in the above-cited references regarding BerkMin, GRASP, chaff, SATO SAT solvers.
Aloul et al. describe a tool for estimating the progress of a SAT solver in “Satometer: How Much Have We Searched?” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, (22:8), August 2003, pages 995-1004. Satometer estimates the percentage of the search space actually explored by a Boolean satisfiability (SAT) solver that uses conflict clause learning. The tool calculates a normalized count for portions of the search-space identified by conflicts. The computation is carried out using a zero-suppressed BDD data structure.